T:Type, d:EqDecider(T), x, y:T. x = y  eqof(d)(x,y) 

latex

Definitions	EqDecider(T), eqof(d), 1of(t), x. t(x), , Prop, b, x:A. B(x), P  Q, P & Q, P  Q, P  Q, t  T
Lemmas	assert wf, iff wf, bool wf, pi1 wf